% !TEX root =  main.tex

\subsection{UMLsec}
\label{sec:UMLSec}

\begin{figure}[t]
	\centering
	\includegraphics[width=\columnwidth]{./figures/UMLsec}
	\caption{UMLsec Y-Process}
	\label{fig:UMLsec}
\end{figure}

J\"urjens proposed \emph{UMLsec}
\cite{springerlink:10.1007/3-540-45314-8-14,springerlink:10.1007/11804192-4},
an annotated \UML model for security modeling and analysis.

\smallskip\noindent \textbf{Security Concerns.}\hspace{0.5cm}  In \emph{UMLsec}, security concerns consist of a set
of threats against application scenarios. For example if we consider mobile systems, the security
requirement \emph{trusted communication} means the system is resilient regarding
various threats of untrusted channels, \eg package lost, data infection, \etc.

\smallskip\noindent \textbf{Modeling.}\hspace{0.5cm}  \emph{UMLsec} uses \emph{\UML Machines} to specify both
business and security models. Security concerns are separated and modeled as an independent
\emph{Adversary Machine}.

Model composition is enabled by means of a mapping, which J\"urjens calls
\emph{renaming}. Renaming associates an \emph{Adversary Machine} the system's
behavioral model by mapping the \textit{stereotypes} with \textit{tags} and
\textit{constraints}. An alternative model composition mechanism is to use a
framework developed by the author which is called \emph{BOLT}. The composed
model is called \emph{Concretized Model} in \emph{UMLsec}.

\smallskip\noindent \textbf{Transformation.}\hspace{0.5cm}  The infrastructure that \emph{UMLsec} produces is a
\emph{Control Flow Graph}. It is produced by transformation from the concretized
model, via a tool called \emph{aiCall}.

\smallskip\noindent \textbf{Analysis.}\hspace{0.5cm}  \emph{UMLsec} allows performing security analysis on the
enforcement infrastructure. The \emph{Control Flow Graph} generated from the concretized
model is compiled to first-order logic axioms which can be verified by the
theorem prover included in the toolset.


Since \emph{UMLsec} models security concerns as \emph{Adversary Machines},
threat risks are analyzed by reasoning on the actions of those adversaries.
In order to perform such reasoning a Prolog-based tool automatically
generates an \emph{attack sequence} attempting to violate the security
requirement. The attack can then be examined to determine and remove the
weakness of system. This mechanism allows traceability of \emph{UMLsec}.

We synthesize in \fig \ref{fig:UMLsec} the \emph{UMLsec} methodology as a specific
\emph{Y-Process} conforming to the Y-Model.


